package at.tasat;

import java.io.PrintStream;

import at.tasat.cnf.Cnf;
import at.tasat.io.OutputFormatter;
import at.tasat.parser.DimacsParser;
import at.tasat.solver.Solver;
import at.tasat.solver.SolverException;

public final class Main {

	public static void main(String[] args) {
		Configuration config = Configuration.get(args);
		int code = main(config);
		System.exit(code);
	}

	public static int main(Configuration config) {
		final PrintStream out = new PrintStream(config.getOut());
		final PrintStream err = new PrintStream(config.getErr());
		try {
			if (config.isVerboseConfig()) {
				out.println(OutputFormatter.getCommentString(config.toString()));
			}

			Cnf cnf = DimacsParser.parse(config.getIn());
			config.getIn().close();
			Solver solver = Solver.create(config.getSolverConfig(), cnf);
			long timeStart = System.currentTimeMillis();
			boolean sat = solver.solve();
			long time = System.currentTimeMillis() - timeStart;
			solver.releaseThreadManager();
			if (config.isVerboseTime()) {
				out.println(OutputFormatter.getCommentString(time + "[ms]"));
			}
			out.println(OutputFormatter.getResultString(sat, solver.getAssignment().getAllAssignments()));

			return 0;
		} catch (SolverException se) {
			err.println(OutputFormatter.getErrorString(se));
			return 1;
		} catch (Throwable error) {
			err.println(OutputFormatter.getErrorString(error));
			return 2;
		}
	}

}
